De Bruijn notation

A variation of lambda notation for specifying functions using

numbers instead of names to refer to formal parameters. A

reference to a formal parameter is a number which gives the

number of lambdas (written as \ here) between the reference

and the lambda which binds the parameter. E.g. the function \

f . \ x . f x would be written \ . \ . 1 0. The 0 refers to

the innermost lambda, the 1 to the next etc. The chief

advantage of this notation is that it avoids the possibility

of name capture and removes the need for alpha conversion.

[N.G. De Bruijn, "Lambda Calculus Notation with Nameless

Dummies: A Tool for Automatic Formula Manipulation, with

Application to the Church-Rosser Theorem", Indag Math. 34, pp

381-392]